$\forall$$T$:Type, $L_{1}$, $L_{2}$:($T$ List).
\\[0ex]no\_repeats($T$;$L_{1}$ @ $L_{2}$) $\Leftarrow\!\Rightarrow$ \{no\_repeats($T$;$L_{1}$) \& no\_repeats($T$;$L_{2}$) \& l\_disjoint($T$;$L_{1}$;$L_{2}$)\}